﻿// Spun AJAX Framework
// Copyright (C) 2008 Blake Hegerle
//
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.IO;

namespace Formality.FormalSystem
{
    public class Variable : Proposition
    {
        public Variable(string Name)
        {
            this.Name = Name;
        }

        public string Name { get; private set; }

        public int BindingNumber { get; set; }
        public bool Bound { get { return BindingNumber > 0; } }

        #region Proposition Overrides
        public override Inference? Matches(Proposition that, Substitution Substitution)
        {
            if (Substitution.HasSubstitution(this))
            {
                if (Substitution[this].Equals(that) == false)
                    return null;
            }
            else
                Substitution[this] = that;

            return new Inference();
        }

        public override Proposition Replace(Substitution Substitution)
        {
            if (Substitution.HasSubstitution(this))
                return Substitution[this];
            else
                return this;
        }
        #endregion

        #region Sentence overrides
        public override bool Equals(Sentence Sentence)
        {
            var that = Sentence as Variable;

            if (that == null)
                return false;

            if (this.Name == that.Name)
            {
                if (this.Bound || that.Bound)
                {
                    return (this.Bound && that.Bound)
                        && (this.BindingNumber == that.BindingNumber);
                }
                else
                {
                    // both free
                    return true;
                }
            }

            return false;
        }

        public override int HashCode
        {
            get { return Name.GetHashCode() ^ BindingNumber; }
        }

        public override void Serialize(TextWriter Writer, bool Detailed)
        {
            Writer.Write(Name);

            if (Detailed && Bound)
                Writer.Write(BindingNumber);
        }

        public override void Bind(Bindings Bindings, int Depth)
        {
            var BoundTo = Bindings[Name];

            if (BoundTo != null)
                BindingNumber = BoundTo.BindingNumber;
        }
        #endregion
    }
}
